Left Termination of the query pattern add_in_3(g, g, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Queries:

add(g,g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(X, Y, Z) → U31(X, Y, Z, addz_in(X, Y, Z))
ADD_IN(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDZ_IN(one(X), one(Y), zero(Z)) → U131(X, Y, Z, addc_in(X, Y, Z))
ADDZ_IN(one(X), one(Y), zero(Z)) → ADDC_IN(X, Y, Z)
ADDC_IN(X, Y, Z) → U161(X, Y, Z, addC_in(X, Y, Z))
ADDC_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDC_IN1(one(X), one(Y), one(Z)) → U261(X, Y, Z, addc_in(X, Y, Z))
ADDC_IN1(one(X), one(Y), one(Z)) → ADDC_IN(X, Y, Z)
ADDC_IN(b, Y, Z) → U151(Y, Z, succZ_in(Y, Z))
ADDC_IN(b, Y, Z) → SUCCZ_IN(Y, Z)
SUCCZ_IN(one(X), zero(Z)) → U341(X, Z, succ_in(X, Z))
SUCCZ_IN(one(X), zero(Z)) → SUCC_IN(X, Z)
SUCC_IN(one(X), zero(Z)) → U321(X, Z, succ_in(X, Z))
SUCC_IN(one(X), zero(Z)) → SUCC_IN(X, Z)
SUCC_IN(zero(X), one(X)) → U311(X, binaryZ_in(X))
SUCC_IN(zero(X), one(X)) → BINARYZ_IN(X)
BINARYZ_IN(one(X)) → U301(X, binary_in(X))
BINARYZ_IN(one(X)) → BINARY_IN(X)
BINARY_IN(one(X)) → U281(X, binary_in(X))
BINARY_IN(one(X)) → BINARY_IN(X)
BINARY_IN(zero(X)) → U271(X, binaryZ_in(X))
BINARY_IN(zero(X)) → BINARYZ_IN(X)
BINARYZ_IN(zero(X)) → U291(X, binaryZ_in(X))
BINARYZ_IN(zero(X)) → BINARYZ_IN(X)
SUCCZ_IN(zero(X), one(X)) → U331(X, binaryZ_in(X))
SUCCZ_IN(zero(X), one(X)) → BINARYZ_IN(X)
ADDC_IN(X, b, Z) → U141(X, Z, succZ_in(X, Z))
ADDC_IN(X, b, Z) → SUCCZ_IN(X, Z)
ADDC_IN1(one(X), zero(Y), zero(Z)) → U251(X, Y, Z, addY_in(X, Y, Z))
ADDC_IN1(one(X), zero(Y), zero(Z)) → ADDY_IN(X, Y, Z)
ADDY_IN(X, Y, Z) → U221(X, Y, Z, addC_in(X, Y, Z))
ADDY_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDC_IN1(zero(X), one(Y), zero(Z)) → U241(X, Y, Z, addX_in(X, Y, Z))
ADDC_IN1(zero(X), one(Y), zero(Z)) → ADDX_IN(X, Y, Z)
ADDX_IN(X, Y, Z) → U191(X, Y, Z, addC_in(X, Y, Z))
ADDX_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDC_IN1(zero(X), zero(Y), one(Z)) → U231(X, Y, Z, addz_in(X, Y, Z))
ADDC_IN1(zero(X), zero(Y), one(Z)) → ADDZ_IN(X, Y, Z)
ADDZ_IN(one(X), zero(Y), one(Z)) → U121(X, Y, Z, addy_in(X, Y, Z))
ADDZ_IN(one(X), zero(Y), one(Z)) → ADDY_IN1(X, Y, Z)
ADDY_IN1(X, Y, Z) → U91(X, Y, Z, addz_in(X, Y, Z))
ADDY_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDZ_IN(zero(X), one(Y), one(Z)) → U111(X, Y, Z, addx_in(X, Y, Z))
ADDZ_IN(zero(X), one(Y), one(Z)) → ADDX_IN1(X, Y, Z)
ADDX_IN1(X, Y, Z) → U61(X, Y, Z, addz_in(X, Y, Z))
ADDX_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDZ_IN(zero(X), zero(Y), zero(Z)) → U101(X, Y, Z, addz_in(X, Y, Z))
ADDZ_IN(zero(X), zero(Y), zero(Z)) → ADDZ_IN(X, Y, Z)
ADDX_IN1(zero(X), b, zero(X)) → U51(X, binaryZ_in(X))
ADDX_IN1(zero(X), b, zero(X)) → BINARYZ_IN(X)
ADDX_IN1(one(X), b, one(X)) → U41(X, binary_in(X))
ADDX_IN1(one(X), b, one(X)) → BINARY_IN(X)
ADDY_IN1(b, zero(Y), zero(Y)) → U81(Y, binaryZ_in(Y))
ADDY_IN1(b, zero(Y), zero(Y)) → BINARYZ_IN(Y)
ADDY_IN1(b, one(Y), one(Y)) → U71(Y, binary_in(Y))
ADDY_IN1(b, one(Y), one(Y)) → BINARY_IN(Y)
ADDX_IN(one(X), b, zero(Z)) → U181(X, Z, succ_in(X, Z))
ADDX_IN(one(X), b, zero(Z)) → SUCC_IN(X, Z)
ADDX_IN(zero(X), b, one(X)) → U171(X, binaryZ_in(X))
ADDX_IN(zero(X), b, one(X)) → BINARYZ_IN(X)
ADDY_IN(b, one(Y), zero(Z)) → U211(Y, Z, succ_in(Y, Z))
ADDY_IN(b, one(Y), zero(Z)) → SUCC_IN(Y, Z)
ADDY_IN(b, zero(Y), one(Y)) → U201(Y, binaryZ_in(Y))
ADDY_IN(b, zero(Y), one(Y)) → BINARYZ_IN(Y)
ADD_IN(b, Y, Y) → U21(Y, binaryZ_in(Y))
ADD_IN(b, Y, Y) → BINARYZ_IN(Y)
ADD_IN(X, b, X) → U11(X, binaryZ_in(X))
ADD_IN(X, b, X) → BINARYZ_IN(X)

The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
U301(x1, x2)  =  U301(x2)
U271(x1, x2)  =  U271(x2)
ADDY_IN(x1, x2, x3)  =  ADDY_IN(x1, x2)
U201(x1, x2)  =  U201(x1, x2)
BINARYZ_IN(x1)  =  BINARYZ_IN(x1)
U41(x1, x2)  =  U41(x1, x2)
U211(x1, x2, x3)  =  U211(x3)
ADDY_IN1(x1, x2, x3)  =  ADDY_IN1(x1, x2)
U261(x1, x2, x3, x4)  =  U261(x4)
U81(x1, x2)  =  U81(x1, x2)
U181(x1, x2, x3)  =  U181(x3)
U221(x1, x2, x3, x4)  =  U221(x4)
U51(x1, x2)  =  U51(x1, x2)
U311(x1, x2)  =  U311(x1, x2)
ADDC_IN1(x1, x2, x3)  =  ADDC_IN1(x1, x2)
U131(x1, x2, x3, x4)  =  U131(x4)
U171(x1, x2)  =  U171(x1, x2)
U11(x1, x2)  =  U11(x1, x2)
U291(x1, x2)  =  U291(x2)
U91(x1, x2, x3, x4)  =  U91(x4)
U141(x1, x2, x3)  =  U141(x3)
U191(x1, x2, x3, x4)  =  U191(x4)
U111(x1, x2, x3, x4)  =  U111(x4)
SUCC_IN(x1, x2)  =  SUCC_IN(x1)
U281(x1, x2)  =  U281(x2)
ADDZ_IN(x1, x2, x3)  =  ADDZ_IN(x1, x2)
U101(x1, x2, x3, x4)  =  U101(x4)
ADDC_IN(x1, x2, x3)  =  ADDC_IN(x1, x2)
U231(x1, x2, x3, x4)  =  U231(x4)
U121(x1, x2, x3, x4)  =  U121(x4)
U21(x1, x2)  =  U21(x1, x2)
U241(x1, x2, x3, x4)  =  U241(x4)
U161(x1, x2, x3, x4)  =  U161(x4)
U331(x1, x2)  =  U331(x1, x2)
U71(x1, x2)  =  U71(x1, x2)
ADDX_IN1(x1, x2, x3)  =  ADDX_IN1(x1, x2)
U31(x1, x2, x3, x4)  =  U31(x4)
U341(x1, x2, x3)  =  U341(x3)
U321(x1, x2, x3)  =  U321(x3)
BINARY_IN(x1)  =  BINARY_IN(x1)
U251(x1, x2, x3, x4)  =  U251(x4)
U61(x1, x2, x3, x4)  =  U61(x4)
ADDX_IN(x1, x2, x3)  =  ADDX_IN(x1, x2)
SUCCZ_IN(x1, x2)  =  SUCCZ_IN(x1)
U151(x1, x2, x3)  =  U151(x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(X, Y, Z) → U31(X, Y, Z, addz_in(X, Y, Z))
ADD_IN(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDZ_IN(one(X), one(Y), zero(Z)) → U131(X, Y, Z, addc_in(X, Y, Z))
ADDZ_IN(one(X), one(Y), zero(Z)) → ADDC_IN(X, Y, Z)
ADDC_IN(X, Y, Z) → U161(X, Y, Z, addC_in(X, Y, Z))
ADDC_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDC_IN1(one(X), one(Y), one(Z)) → U261(X, Y, Z, addc_in(X, Y, Z))
ADDC_IN1(one(X), one(Y), one(Z)) → ADDC_IN(X, Y, Z)
ADDC_IN(b, Y, Z) → U151(Y, Z, succZ_in(Y, Z))
ADDC_IN(b, Y, Z) → SUCCZ_IN(Y, Z)
SUCCZ_IN(one(X), zero(Z)) → U341(X, Z, succ_in(X, Z))
SUCCZ_IN(one(X), zero(Z)) → SUCC_IN(X, Z)
SUCC_IN(one(X), zero(Z)) → U321(X, Z, succ_in(X, Z))
SUCC_IN(one(X), zero(Z)) → SUCC_IN(X, Z)
SUCC_IN(zero(X), one(X)) → U311(X, binaryZ_in(X))
SUCC_IN(zero(X), one(X)) → BINARYZ_IN(X)
BINARYZ_IN(one(X)) → U301(X, binary_in(X))
BINARYZ_IN(one(X)) → BINARY_IN(X)
BINARY_IN(one(X)) → U281(X, binary_in(X))
BINARY_IN(one(X)) → BINARY_IN(X)
BINARY_IN(zero(X)) → U271(X, binaryZ_in(X))
BINARY_IN(zero(X)) → BINARYZ_IN(X)
BINARYZ_IN(zero(X)) → U291(X, binaryZ_in(X))
BINARYZ_IN(zero(X)) → BINARYZ_IN(X)
SUCCZ_IN(zero(X), one(X)) → U331(X, binaryZ_in(X))
SUCCZ_IN(zero(X), one(X)) → BINARYZ_IN(X)
ADDC_IN(X, b, Z) → U141(X, Z, succZ_in(X, Z))
ADDC_IN(X, b, Z) → SUCCZ_IN(X, Z)
ADDC_IN1(one(X), zero(Y), zero(Z)) → U251(X, Y, Z, addY_in(X, Y, Z))
ADDC_IN1(one(X), zero(Y), zero(Z)) → ADDY_IN(X, Y, Z)
ADDY_IN(X, Y, Z) → U221(X, Y, Z, addC_in(X, Y, Z))
ADDY_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDC_IN1(zero(X), one(Y), zero(Z)) → U241(X, Y, Z, addX_in(X, Y, Z))
ADDC_IN1(zero(X), one(Y), zero(Z)) → ADDX_IN(X, Y, Z)
ADDX_IN(X, Y, Z) → U191(X, Y, Z, addC_in(X, Y, Z))
ADDX_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDC_IN1(zero(X), zero(Y), one(Z)) → U231(X, Y, Z, addz_in(X, Y, Z))
ADDC_IN1(zero(X), zero(Y), one(Z)) → ADDZ_IN(X, Y, Z)
ADDZ_IN(one(X), zero(Y), one(Z)) → U121(X, Y, Z, addy_in(X, Y, Z))
ADDZ_IN(one(X), zero(Y), one(Z)) → ADDY_IN1(X, Y, Z)
ADDY_IN1(X, Y, Z) → U91(X, Y, Z, addz_in(X, Y, Z))
ADDY_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDZ_IN(zero(X), one(Y), one(Z)) → U111(X, Y, Z, addx_in(X, Y, Z))
ADDZ_IN(zero(X), one(Y), one(Z)) → ADDX_IN1(X, Y, Z)
ADDX_IN1(X, Y, Z) → U61(X, Y, Z, addz_in(X, Y, Z))
ADDX_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDZ_IN(zero(X), zero(Y), zero(Z)) → U101(X, Y, Z, addz_in(X, Y, Z))
ADDZ_IN(zero(X), zero(Y), zero(Z)) → ADDZ_IN(X, Y, Z)
ADDX_IN1(zero(X), b, zero(X)) → U51(X, binaryZ_in(X))
ADDX_IN1(zero(X), b, zero(X)) → BINARYZ_IN(X)
ADDX_IN1(one(X), b, one(X)) → U41(X, binary_in(X))
ADDX_IN1(one(X), b, one(X)) → BINARY_IN(X)
ADDY_IN1(b, zero(Y), zero(Y)) → U81(Y, binaryZ_in(Y))
ADDY_IN1(b, zero(Y), zero(Y)) → BINARYZ_IN(Y)
ADDY_IN1(b, one(Y), one(Y)) → U71(Y, binary_in(Y))
ADDY_IN1(b, one(Y), one(Y)) → BINARY_IN(Y)
ADDX_IN(one(X), b, zero(Z)) → U181(X, Z, succ_in(X, Z))
ADDX_IN(one(X), b, zero(Z)) → SUCC_IN(X, Z)
ADDX_IN(zero(X), b, one(X)) → U171(X, binaryZ_in(X))
ADDX_IN(zero(X), b, one(X)) → BINARYZ_IN(X)
ADDY_IN(b, one(Y), zero(Z)) → U211(Y, Z, succ_in(Y, Z))
ADDY_IN(b, one(Y), zero(Z)) → SUCC_IN(Y, Z)
ADDY_IN(b, zero(Y), one(Y)) → U201(Y, binaryZ_in(Y))
ADDY_IN(b, zero(Y), one(Y)) → BINARYZ_IN(Y)
ADD_IN(b, Y, Y) → U21(Y, binaryZ_in(Y))
ADD_IN(b, Y, Y) → BINARYZ_IN(Y)
ADD_IN(X, b, X) → U11(X, binaryZ_in(X))
ADD_IN(X, b, X) → BINARYZ_IN(X)

The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
U301(x1, x2)  =  U301(x2)
U271(x1, x2)  =  U271(x2)
ADDY_IN(x1, x2, x3)  =  ADDY_IN(x1, x2)
U201(x1, x2)  =  U201(x1, x2)
BINARYZ_IN(x1)  =  BINARYZ_IN(x1)
U41(x1, x2)  =  U41(x1, x2)
U211(x1, x2, x3)  =  U211(x3)
ADDY_IN1(x1, x2, x3)  =  ADDY_IN1(x1, x2)
U261(x1, x2, x3, x4)  =  U261(x4)
U81(x1, x2)  =  U81(x1, x2)
U181(x1, x2, x3)  =  U181(x3)
U221(x1, x2, x3, x4)  =  U221(x4)
U51(x1, x2)  =  U51(x1, x2)
U311(x1, x2)  =  U311(x1, x2)
ADDC_IN1(x1, x2, x3)  =  ADDC_IN1(x1, x2)
U131(x1, x2, x3, x4)  =  U131(x4)
U171(x1, x2)  =  U171(x1, x2)
U11(x1, x2)  =  U11(x1, x2)
U291(x1, x2)  =  U291(x2)
U91(x1, x2, x3, x4)  =  U91(x4)
U141(x1, x2, x3)  =  U141(x3)
U191(x1, x2, x3, x4)  =  U191(x4)
U111(x1, x2, x3, x4)  =  U111(x4)
SUCC_IN(x1, x2)  =  SUCC_IN(x1)
U281(x1, x2)  =  U281(x2)
ADDZ_IN(x1, x2, x3)  =  ADDZ_IN(x1, x2)
U101(x1, x2, x3, x4)  =  U101(x4)
ADDC_IN(x1, x2, x3)  =  ADDC_IN(x1, x2)
U231(x1, x2, x3, x4)  =  U231(x4)
U121(x1, x2, x3, x4)  =  U121(x4)
U21(x1, x2)  =  U21(x1, x2)
U241(x1, x2, x3, x4)  =  U241(x4)
U161(x1, x2, x3, x4)  =  U161(x4)
U331(x1, x2)  =  U331(x1, x2)
U71(x1, x2)  =  U71(x1, x2)
ADDX_IN1(x1, x2, x3)  =  ADDX_IN1(x1, x2)
U31(x1, x2, x3, x4)  =  U31(x4)
U341(x1, x2, x3)  =  U341(x3)
U321(x1, x2, x3)  =  U321(x3)
BINARY_IN(x1)  =  BINARY_IN(x1)
U251(x1, x2, x3, x4)  =  U251(x4)
U61(x1, x2, x3, x4)  =  U61(x4)
ADDX_IN(x1, x2, x3)  =  ADDX_IN(x1, x2)
SUCCZ_IN(x1, x2)  =  SUCCZ_IN(x1)
U151(x1, x2, x3)  =  U151(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 3 SCCs with 50 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

BINARYZ_IN(one(X)) → BINARY_IN(X)
BINARYZ_IN(zero(X)) → BINARYZ_IN(X)
BINARY_IN(one(X)) → BINARY_IN(X)
BINARY_IN(zero(X)) → BINARYZ_IN(X)

The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)
BINARYZ_IN(x1)  =  BINARYZ_IN(x1)
BINARY_IN(x1)  =  BINARY_IN(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

BINARYZ_IN(one(X)) → BINARY_IN(X)
BINARYZ_IN(zero(X)) → BINARYZ_IN(X)
BINARY_IN(one(X)) → BINARY_IN(X)
BINARY_IN(zero(X)) → BINARYZ_IN(X)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

BINARYZ_IN(one(X)) → BINARY_IN(X)
BINARYZ_IN(zero(X)) → BINARYZ_IN(X)
BINARY_IN(one(X)) → BINARY_IN(X)
BINARY_IN(zero(X)) → BINARYZ_IN(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SUCC_IN(one(X), zero(Z)) → SUCC_IN(X, Z)

The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)
SUCC_IN(x1, x2)  =  SUCC_IN(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SUCC_IN(one(X), zero(Z)) → SUCC_IN(X, Z)

R is empty.
The argument filtering Pi contains the following mapping:
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
SUCC_IN(x1, x2)  =  SUCC_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SUCC_IN(one(X)) → SUCC_IN(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

ADDC_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDX_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDC_IN1(one(X), zero(Y), zero(Z)) → ADDY_IN(X, Y, Z)
ADDC_IN1(one(X), one(Y), one(Z)) → ADDC_IN(X, Y, Z)
ADDZ_IN(zero(X), zero(Y), zero(Z)) → ADDZ_IN(X, Y, Z)
ADDC_IN1(zero(X), zero(Y), one(Z)) → ADDZ_IN(X, Y, Z)
ADDY_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDY_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDX_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDZ_IN(one(X), zero(Y), one(Z)) → ADDY_IN1(X, Y, Z)
ADDZ_IN(one(X), one(Y), zero(Z)) → ADDC_IN(X, Y, Z)
ADDC_IN1(zero(X), one(Y), zero(Z)) → ADDX_IN(X, Y, Z)
ADDZ_IN(zero(X), one(Y), one(Z)) → ADDX_IN1(X, Y, Z)

The TRS R consists of the following rules:

add_in(X, Y, Z) → U3(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), one(Y), zero(Z)) → U13(X, Y, Z, addc_in(X, Y, Z))
addc_in(X, Y, Z) → U16(X, Y, Z, addC_in(X, Y, Z))
addC_in(one(X), one(Y), one(Z)) → U26(X, Y, Z, addc_in(X, Y, Z))
addc_in(b, Y, Z) → U15(Y, Z, succZ_in(Y, Z))
succZ_in(one(X), zero(Z)) → U34(X, Z, succ_in(X, Z))
succ_in(one(X), zero(Z)) → U32(X, Z, succ_in(X, Z))
succ_in(zero(X), one(X)) → U31(X, binaryZ_in(X))
binaryZ_in(one(X)) → U30(X, binary_in(X))
binary_in(one(X)) → U28(X, binary_in(X))
binary_in(zero(X)) → U27(X, binaryZ_in(X))
binaryZ_in(zero(X)) → U29(X, binaryZ_in(X))
U29(X, binaryZ_out(X)) → binaryZ_out(zero(X))
U27(X, binaryZ_out(X)) → binary_out(zero(X))
binary_in(b) → binary_out(b)
U28(X, binary_out(X)) → binary_out(one(X))
U30(X, binary_out(X)) → binaryZ_out(one(X))
U31(X, binaryZ_out(X)) → succ_out(zero(X), one(X))
succ_in(b, one(b)) → succ_out(b, one(b))
U32(X, Z, succ_out(X, Z)) → succ_out(one(X), zero(Z))
U34(X, Z, succ_out(X, Z)) → succZ_out(one(X), zero(Z))
succZ_in(zero(X), one(X)) → U33(X, binaryZ_in(X))
U33(X, binaryZ_out(X)) → succZ_out(zero(X), one(X))
U15(Y, Z, succZ_out(Y, Z)) → addc_out(b, Y, Z)
addc_in(X, b, Z) → U14(X, Z, succZ_in(X, Z))
U14(X, Z, succZ_out(X, Z)) → addc_out(X, b, Z)
addc_in(b, b, one(b)) → addc_out(b, b, one(b))
U26(X, Y, Z, addc_out(X, Y, Z)) → addC_out(one(X), one(Y), one(Z))
addC_in(one(X), zero(Y), zero(Z)) → U25(X, Y, Z, addY_in(X, Y, Z))
addY_in(X, Y, Z) → U22(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), one(Y), zero(Z)) → U24(X, Y, Z, addX_in(X, Y, Z))
addX_in(X, Y, Z) → U19(X, Y, Z, addC_in(X, Y, Z))
addC_in(zero(X), zero(Y), one(Z)) → U23(X, Y, Z, addz_in(X, Y, Z))
addz_in(one(X), zero(Y), one(Z)) → U12(X, Y, Z, addy_in(X, Y, Z))
addy_in(X, Y, Z) → U9(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), one(Y), one(Z)) → U11(X, Y, Z, addx_in(X, Y, Z))
addx_in(X, Y, Z) → U6(X, Y, Z, addz_in(X, Y, Z))
addz_in(zero(X), zero(Y), zero(Z)) → U10(X, Y, Z, addz_in(X, Y, Z))
U10(X, Y, Z, addz_out(X, Y, Z)) → addz_out(zero(X), zero(Y), zero(Z))
U6(X, Y, Z, addz_out(X, Y, Z)) → addx_out(X, Y, Z)
addx_in(zero(X), b, zero(X)) → U5(X, binaryZ_in(X))
U5(X, binaryZ_out(X)) → addx_out(zero(X), b, zero(X))
addx_in(one(X), b, one(X)) → U4(X, binary_in(X))
U4(X, binary_out(X)) → addx_out(one(X), b, one(X))
U11(X, Y, Z, addx_out(X, Y, Z)) → addz_out(zero(X), one(Y), one(Z))
U9(X, Y, Z, addz_out(X, Y, Z)) → addy_out(X, Y, Z)
addy_in(b, zero(Y), zero(Y)) → U8(Y, binaryZ_in(Y))
U8(Y, binaryZ_out(Y)) → addy_out(b, zero(Y), zero(Y))
addy_in(b, one(Y), one(Y)) → U7(Y, binary_in(Y))
U7(Y, binary_out(Y)) → addy_out(b, one(Y), one(Y))
U12(X, Y, Z, addy_out(X, Y, Z)) → addz_out(one(X), zero(Y), one(Z))
U23(X, Y, Z, addz_out(X, Y, Z)) → addC_out(zero(X), zero(Y), one(Z))
U19(X, Y, Z, addC_out(X, Y, Z)) → addX_out(X, Y, Z)
addX_in(one(X), b, zero(Z)) → U18(X, Z, succ_in(X, Z))
U18(X, Z, succ_out(X, Z)) → addX_out(one(X), b, zero(Z))
addX_in(zero(X), b, one(X)) → U17(X, binaryZ_in(X))
U17(X, binaryZ_out(X)) → addX_out(zero(X), b, one(X))
U24(X, Y, Z, addX_out(X, Y, Z)) → addC_out(zero(X), one(Y), zero(Z))
U22(X, Y, Z, addC_out(X, Y, Z)) → addY_out(X, Y, Z)
addY_in(b, one(Y), zero(Z)) → U21(Y, Z, succ_in(Y, Z))
U21(Y, Z, succ_out(Y, Z)) → addY_out(b, one(Y), zero(Z))
addY_in(b, zero(Y), one(Y)) → U20(Y, binaryZ_in(Y))
U20(Y, binaryZ_out(Y)) → addY_out(b, zero(Y), one(Y))
U25(X, Y, Z, addY_out(X, Y, Z)) → addC_out(one(X), zero(Y), zero(Z))
U16(X, Y, Z, addC_out(X, Y, Z)) → addc_out(X, Y, Z)
U13(X, Y, Z, addc_out(X, Y, Z)) → addz_out(one(X), one(Y), zero(Z))
U3(X, Y, Z, addz_out(X, Y, Z)) → add_out(X, Y, Z)
add_in(b, Y, Y) → U2(Y, binaryZ_in(Y))
U2(Y, binaryZ_out(Y)) → add_out(b, Y, Y)
add_in(X, b, X) → U1(X, binaryZ_in(X))
U1(X, binaryZ_out(X)) → add_out(X, b, X)
add_in(b, b, b) → add_out(b, b, b)

The argument filtering Pi contains the following mapping:
add_in(x1, x2, x3)  =  add_in(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
addz_in(x1, x2, x3)  =  addz_in(x1, x2)
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
U13(x1, x2, x3, x4)  =  U13(x4)
addc_in(x1, x2, x3)  =  addc_in(x1, x2)
U16(x1, x2, x3, x4)  =  U16(x4)
addC_in(x1, x2, x3)  =  addC_in(x1, x2)
U26(x1, x2, x3, x4)  =  U26(x4)
b  =  b
U15(x1, x2, x3)  =  U15(x3)
succZ_in(x1, x2)  =  succZ_in(x1)
U34(x1, x2, x3)  =  U34(x3)
succ_in(x1, x2)  =  succ_in(x1)
U32(x1, x2, x3)  =  U32(x3)
U31(x1, x2)  =  U31(x1, x2)
binaryZ_in(x1)  =  binaryZ_in(x1)
U30(x1, x2)  =  U30(x2)
binary_in(x1)  =  binary_in(x1)
U28(x1, x2)  =  U28(x2)
U27(x1, x2)  =  U27(x2)
U29(x1, x2)  =  U29(x2)
binaryZ_out(x1)  =  binaryZ_out
binary_out(x1)  =  binary_out
succ_out(x1, x2)  =  succ_out(x2)
succZ_out(x1, x2)  =  succZ_out(x2)
U33(x1, x2)  =  U33(x1, x2)
addc_out(x1, x2, x3)  =  addc_out(x3)
U14(x1, x2, x3)  =  U14(x3)
addC_out(x1, x2, x3)  =  addC_out(x3)
U25(x1, x2, x3, x4)  =  U25(x4)
addY_in(x1, x2, x3)  =  addY_in(x1, x2)
U22(x1, x2, x3, x4)  =  U22(x4)
U24(x1, x2, x3, x4)  =  U24(x4)
addX_in(x1, x2, x3)  =  addX_in(x1, x2)
U19(x1, x2, x3, x4)  =  U19(x4)
U23(x1, x2, x3, x4)  =  U23(x4)
U12(x1, x2, x3, x4)  =  U12(x4)
addy_in(x1, x2, x3)  =  addy_in(x1, x2)
U9(x1, x2, x3, x4)  =  U9(x4)
U11(x1, x2, x3, x4)  =  U11(x4)
addx_in(x1, x2, x3)  =  addx_in(x1, x2)
U6(x1, x2, x3, x4)  =  U6(x4)
U10(x1, x2, x3, x4)  =  U10(x4)
addz_out(x1, x2, x3)  =  addz_out(x3)
addx_out(x1, x2, x3)  =  addx_out(x3)
U5(x1, x2)  =  U5(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
addy_out(x1, x2, x3)  =  addy_out(x3)
U8(x1, x2)  =  U8(x1, x2)
U7(x1, x2)  =  U7(x1, x2)
addX_out(x1, x2, x3)  =  addX_out(x3)
U18(x1, x2, x3)  =  U18(x3)
U17(x1, x2)  =  U17(x1, x2)
addY_out(x1, x2, x3)  =  addY_out(x3)
U21(x1, x2, x3)  =  U21(x3)
U20(x1, x2)  =  U20(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U2(x1, x2)  =  U2(x1, x2)
U1(x1, x2)  =  U1(x1, x2)
ADDY_IN(x1, x2, x3)  =  ADDY_IN(x1, x2)
ADDY_IN1(x1, x2, x3)  =  ADDY_IN1(x1, x2)
ADDC_IN1(x1, x2, x3)  =  ADDC_IN1(x1, x2)
ADDZ_IN(x1, x2, x3)  =  ADDZ_IN(x1, x2)
ADDC_IN(x1, x2, x3)  =  ADDC_IN(x1, x2)
ADDX_IN1(x1, x2, x3)  =  ADDX_IN1(x1, x2)
ADDX_IN(x1, x2, x3)  =  ADDX_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ADDC_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDX_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDC_IN1(one(X), zero(Y), zero(Z)) → ADDY_IN(X, Y, Z)
ADDC_IN1(one(X), one(Y), one(Z)) → ADDC_IN(X, Y, Z)
ADDZ_IN(zero(X), zero(Y), zero(Z)) → ADDZ_IN(X, Y, Z)
ADDC_IN1(zero(X), zero(Y), one(Z)) → ADDZ_IN(X, Y, Z)
ADDY_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDY_IN1(X, Y, Z) → ADDZ_IN(X, Y, Z)
ADDX_IN(X, Y, Z) → ADDC_IN1(X, Y, Z)
ADDZ_IN(one(X), zero(Y), one(Z)) → ADDY_IN1(X, Y, Z)
ADDZ_IN(one(X), one(Y), zero(Z)) → ADDC_IN(X, Y, Z)
ADDC_IN1(zero(X), one(Y), zero(Z)) → ADDX_IN(X, Y, Z)
ADDZ_IN(zero(X), one(Y), one(Z)) → ADDX_IN1(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
one(x1)  =  one(x1)
zero(x1)  =  zero(x1)
ADDY_IN(x1, x2, x3)  =  ADDY_IN(x1, x2)
ADDY_IN1(x1, x2, x3)  =  ADDY_IN1(x1, x2)
ADDC_IN1(x1, x2, x3)  =  ADDC_IN1(x1, x2)
ADDZ_IN(x1, x2, x3)  =  ADDZ_IN(x1, x2)
ADDC_IN(x1, x2, x3)  =  ADDC_IN(x1, x2)
ADDX_IN1(x1, x2, x3)  =  ADDX_IN1(x1, x2)
ADDX_IN(x1, x2, x3)  =  ADDX_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

ADDC_IN(X, Y) → ADDC_IN1(X, Y)
ADDY_IN1(X, Y) → ADDZ_IN(X, Y)
ADDZ_IN(one(X), zero(Y)) → ADDY_IN1(X, Y)
ADDZ_IN(one(X), one(Y)) → ADDC_IN(X, Y)
ADDY_IN(X, Y) → ADDC_IN1(X, Y)
ADDC_IN1(one(X), one(Y)) → ADDC_IN(X, Y)
ADDZ_IN(zero(X), zero(Y)) → ADDZ_IN(X, Y)
ADDC_IN1(zero(X), zero(Y)) → ADDZ_IN(X, Y)
ADDZ_IN(zero(X), one(Y)) → ADDX_IN1(X, Y)
ADDX_IN(X, Y) → ADDC_IN1(X, Y)
ADDC_IN1(zero(X), one(Y)) → ADDX_IN(X, Y)
ADDC_IN1(one(X), zero(Y)) → ADDY_IN(X, Y)
ADDX_IN1(X, Y) → ADDZ_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: